Termination w.r.t. Q proof of TRS/Rubioselsort.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(Y)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
le(0, Y) → true
le(s(X), 0) → false
le(s(X), s(Y)) → le(X, Y)
min(cons(0, nil)) → 0
min(cons(s(N), nil)) → s(N)
min(cons(N, cons(M, L))) → ifmin(le(N, M), cons(N, cons(M, L)))
ifmin(true, cons(N, cons(M, L))) → min(cons(N, L))
ifmin(false, cons(N, cons(M, L))) → min(cons(M, L))
replace(N, M, nil) → nil
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L))
ifrepl(true, N, M, cons(K, L)) → cons(M, L)
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L))
selsort(nil) → nil
selsort(cons(N, L)) → ifselsort(eq(N, min(cons(N, L))), cons(N, L))
ifselsort(true, cons(N, L)) → cons(N, selsort(L))
ifselsort(false, cons(N, L)) → cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L)))

Q is empty.

↳ QTRS

  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(Y)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
le(0, Y) → true
le(s(X), 0) → false
le(s(X), s(Y)) → le(X, Y)
min(cons(0, nil)) → 0
min(cons(s(N), nil)) → s(N)
min(cons(N, cons(M, L))) → ifmin(le(N, M), cons(N, cons(M, L)))
ifmin(true, cons(N, cons(M, L))) → min(cons(N, L))
ifmin(false, cons(N, cons(M, L))) → min(cons(M, L))
replace(N, M, nil) → nil
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L))
ifrepl(true, N, M, cons(K, L)) → cons(M, L)
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L))
selsort(nil) → nil
selsort(cons(N, L)) → ifselsort(eq(N, min(cons(N, L))), cons(N, L))
ifselsort(true, cons(N, L)) → cons(N, selsort(L))
ifselsort(false, cons(N, L)) → cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L)))

Q is empty.

The TRS is overlay and locally confluent. By [15] we can switch to innermost.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(Y)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
le(0, Y) → true
le(s(X), 0) → false
le(s(X), s(Y)) → le(X, Y)
min(cons(0, nil)) → 0
min(cons(s(N), nil)) → s(N)
min(cons(N, cons(M, L))) → ifmin(le(N, M), cons(N, cons(M, L)))
ifmin(true, cons(N, cons(M, L))) → min(cons(N, L))
ifmin(false, cons(N, cons(M, L))) → min(cons(M, L))
replace(N, M, nil) → nil
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L))
ifrepl(true, N, M, cons(K, L)) → cons(M, L)
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L))
selsort(nil) → nil
selsort(cons(N, L)) → ifselsort(eq(N, min(cons(N, L))), cons(N, L))
ifselsort(true, cons(N, L)) → cons(N, selsort(L))
ifselsort(false, cons(N, L)) → cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
ifmin(true, cons(x0, cons(x1, x2)))
ifmin(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
ifrepl(true, x0, x1, cons(x2, x3))
ifrepl(false, x0, x1, cons(x2, x3))
selsort(nil)
selsort(cons(x0, x1))
ifselsort(true, cons(x0, x1))
ifselsort(false, cons(x0, x1))

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

MIN(cons(N, cons(M, L))) → LE(N, M)
IFMIN(true, cons(N, cons(M, L))) → MIN(cons(N, L))
IFREPL(false, N, M, cons(K, L)) → REPLACE(N, M, L)
REPLACE(N, M, cons(K, L)) → EQ(N, K)
REPLACE(N, M, cons(K, L)) → IFREPL(eq(N, K), N, M, cons(K, L))
IFSELSORT(false, cons(N, L)) → SELSORT(replace(min(cons(N, L)), N, L))
IFMIN(false, cons(N, cons(M, L))) → MIN(cons(M, L))
SELSORT(cons(N, L)) → EQ(N, min(cons(N, L)))
EQ(s(X), s(Y)) → EQ(X, Y)
SELSORT(cons(N, L)) → MIN(cons(N, L))
IFSELSORT(false, cons(N, L)) → REPLACE(min(cons(N, L)), N, L)
LE(s(X), s(Y)) → LE(X, Y)
IFSELSORT(true, cons(N, L)) → SELSORT(L)
MIN(cons(N, cons(M, L))) → IFMIN(le(N, M), cons(N, cons(M, L)))
IFSELSORT(false, cons(N, L)) → MIN(cons(N, L))
SELSORT(cons(N, L)) → IFSELSORT(eq(N, min(cons(N, L))), cons(N, L))

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(Y)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
le(0, Y) → true
le(s(X), 0) → false
le(s(X), s(Y)) → le(X, Y)
min(cons(0, nil)) → 0
min(cons(s(N), nil)) → s(N)
min(cons(N, cons(M, L))) → ifmin(le(N, M), cons(N, cons(M, L)))
ifmin(true, cons(N, cons(M, L))) → min(cons(N, L))
ifmin(false, cons(N, cons(M, L))) → min(cons(M, L))
replace(N, M, nil) → nil
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L))
ifrepl(true, N, M, cons(K, L)) → cons(M, L)
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L))
selsort(nil) → nil
selsort(cons(N, L)) → ifselsort(eq(N, min(cons(N, L))), cons(N, L))
ifselsort(true, cons(N, L)) → cons(N, selsort(L))
ifselsort(false, cons(N, L)) → cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
ifmin(true, cons(x0, cons(x1, x2)))
ifmin(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
ifrepl(true, x0, x1, cons(x2, x3))
ifrepl(false, x0, x1, cons(x2, x3))
selsort(nil)
selsort(cons(x0, x1))
ifselsort(true, cons(x0, x1))
ifselsort(false, cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

Q DP problem:
The TRS P consists of the following rules:

MIN(cons(N, cons(M, L))) → LE(N, M)
IFMIN(true, cons(N, cons(M, L))) → MIN(cons(N, L))
IFREPL(false, N, M, cons(K, L)) → REPLACE(N, M, L)
REPLACE(N, M, cons(K, L)) → EQ(N, K)
REPLACE(N, M, cons(K, L)) → IFREPL(eq(N, K), N, M, cons(K, L))
IFSELSORT(false, cons(N, L)) → SELSORT(replace(min(cons(N, L)), N, L))
IFMIN(false, cons(N, cons(M, L))) → MIN(cons(M, L))
SELSORT(cons(N, L)) → EQ(N, min(cons(N, L)))
EQ(s(X), s(Y)) → EQ(X, Y)
SELSORT(cons(N, L)) → MIN(cons(N, L))
IFSELSORT(false, cons(N, L)) → REPLACE(min(cons(N, L)), N, L)
LE(s(X), s(Y)) → LE(X, Y)
IFSELSORT(true, cons(N, L)) → SELSORT(L)
MIN(cons(N, cons(M, L))) → IFMIN(le(N, M), cons(N, cons(M, L)))
IFSELSORT(false, cons(N, L)) → MIN(cons(N, L))
SELSORT(cons(N, L)) → IFSELSORT(eq(N, min(cons(N, L))), cons(N, L))

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(Y)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
le(0, Y) → true
le(s(X), 0) → false
le(s(X), s(Y)) → le(X, Y)
min(cons(0, nil)) → 0
min(cons(s(N), nil)) → s(N)
min(cons(N, cons(M, L))) → ifmin(le(N, M), cons(N, cons(M, L)))
ifmin(true, cons(N, cons(M, L))) → min(cons(N, L))
ifmin(false, cons(N, cons(M, L))) → min(cons(M, L))
replace(N, M, nil) → nil
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L))
ifrepl(true, N, M, cons(K, L)) → cons(M, L)
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L))
selsort(nil) → nil
selsort(cons(N, L)) → ifselsort(eq(N, min(cons(N, L))), cons(N, L))
ifselsort(true, cons(N, L)) → cons(N, selsort(L))
ifselsort(false, cons(N, L)) → cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
ifmin(true, cons(x0, cons(x1, x2)))
ifmin(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
ifrepl(true, x0, x1, cons(x2, x3))
ifrepl(false, x0, x1, cons(x2, x3))
selsort(nil)
selsort(cons(x0, x1))
ifselsort(true, cons(x0, x1))
ifselsort(false, cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted some edges using various graph approximations

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

MIN(cons(N, cons(M, L))) → LE(N, M)
IFREPL(false, N, M, cons(K, L)) → REPLACE(N, M, L)
IFMIN(true, cons(N, cons(M, L))) → MIN(cons(N, L))
REPLACE(N, M, cons(K, L)) → EQ(N, K)
REPLACE(N, M, cons(K, L)) → IFREPL(eq(N, K), N, M, cons(K, L))
IFSELSORT(false, cons(N, L)) → SELSORT(replace(min(cons(N, L)), N, L))
IFMIN(false, cons(N, cons(M, L))) → MIN(cons(M, L))
SELSORT(cons(N, L)) → EQ(N, min(cons(N, L)))
EQ(s(X), s(Y)) → EQ(X, Y)
SELSORT(cons(N, L)) → MIN(cons(N, L))
LE(s(X), s(Y)) → LE(X, Y)
IFSELSORT(false, cons(N, L)) → REPLACE(min(cons(N, L)), N, L)
IFSELSORT(true, cons(N, L)) → SELSORT(L)
MIN(cons(N, cons(M, L))) → IFMIN(le(N, M), cons(N, cons(M, L)))
IFSELSORT(false, cons(N, L)) → MIN(cons(N, L))
SELSORT(cons(N, L)) → IFSELSORT(eq(N, min(cons(N, L))), cons(N, L))

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(Y)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
le(0, Y) → true
le(s(X), 0) → false
le(s(X), s(Y)) → le(X, Y)
min(cons(0, nil)) → 0
min(cons(s(N), nil)) → s(N)
min(cons(N, cons(M, L))) → ifmin(le(N, M), cons(N, cons(M, L)))
ifmin(true, cons(N, cons(M, L))) → min(cons(N, L))
ifmin(false, cons(N, cons(M, L))) → min(cons(M, L))
replace(N, M, nil) → nil
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L))
ifrepl(true, N, M, cons(K, L)) → cons(M, L)
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L))
selsort(nil) → nil
selsort(cons(N, L)) → ifselsort(eq(N, min(cons(N, L))), cons(N, L))
ifselsort(true, cons(N, L)) → cons(N, selsort(L))
ifselsort(false, cons(N, L)) → cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
ifmin(true, cons(x0, cons(x1, x2)))
ifmin(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
ifrepl(true, x0, x1, cons(x2, x3))
ifrepl(false, x0, x1, cons(x2, x3))
selsort(nil)
selsort(cons(x0, x1))
ifselsort(true, cons(x0, x1))
ifselsort(false, cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 5 SCCs with 6 less nodes.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

LE(s(X), s(Y)) → LE(X, Y)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(Y)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
le(0, Y) → true
le(s(X), 0) → false
le(s(X), s(Y)) → le(X, Y)
min(cons(0, nil)) → 0
min(cons(s(N), nil)) → s(N)
min(cons(N, cons(M, L))) → ifmin(le(N, M), cons(N, cons(M, L)))
ifmin(true, cons(N, cons(M, L))) → min(cons(N, L))
ifmin(false, cons(N, cons(M, L))) → min(cons(M, L))
replace(N, M, nil) → nil
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L))
ifrepl(true, N, M, cons(K, L)) → cons(M, L)
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L))
selsort(nil) → nil
selsort(cons(N, L)) → ifselsort(eq(N, min(cons(N, L))), cons(N, L))
ifselsort(true, cons(N, L)) → cons(N, selsort(L))
ifselsort(false, cons(N, L)) → cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
ifmin(true, cons(x0, cons(x1, x2)))
ifmin(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
ifrepl(true, x0, x1, cons(x2, x3))
ifrepl(false, x0, x1, cons(x2, x3))
selsort(nil)
selsort(cons(x0, x1))
ifselsort(true, cons(x0, x1))
ifselsort(false, cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

LE(s(X), s(Y)) → LE(X, Y)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
LE(x1, x2) = LE(x2)
s(x1) = s(x1)

Lexicographic path order with status [19].
Quasi-Precedence:

s₁ > LE₁

Status:

LE₁: [1]
s₁: [1]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(Y)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
le(0, Y) → true
le(s(X), 0) → false
le(s(X), s(Y)) → le(X, Y)
min(cons(0, nil)) → 0
min(cons(s(N), nil)) → s(N)
min(cons(N, cons(M, L))) → ifmin(le(N, M), cons(N, cons(M, L)))
ifmin(true, cons(N, cons(M, L))) → min(cons(N, L))
ifmin(false, cons(N, cons(M, L))) → min(cons(M, L))
replace(N, M, nil) → nil
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L))
ifrepl(true, N, M, cons(K, L)) → cons(M, L)
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L))
selsort(nil) → nil
selsort(cons(N, L)) → ifselsort(eq(N, min(cons(N, L))), cons(N, L))
ifselsort(true, cons(N, L)) → cons(N, selsort(L))
ifselsort(false, cons(N, L)) → cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
ifmin(true, cons(x0, cons(x1, x2)))
ifmin(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
ifrepl(true, x0, x1, cons(x2, x3))
ifrepl(false, x0, x1, cons(x2, x3))
selsort(nil)
selsort(cons(x0, x1))
ifselsort(true, cons(x0, x1))
ifselsort(false, cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IFMIN(false, cons(N, cons(M, L))) → MIN(cons(M, L))
IFMIN(true, cons(N, cons(M, L))) → MIN(cons(N, L))
MIN(cons(N, cons(M, L))) → IFMIN(le(N, M), cons(N, cons(M, L)))

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(Y)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
le(0, Y) → true
le(s(X), 0) → false
le(s(X), s(Y)) → le(X, Y)
min(cons(0, nil)) → 0
min(cons(s(N), nil)) → s(N)
min(cons(N, cons(M, L))) → ifmin(le(N, M), cons(N, cons(M, L)))
ifmin(true, cons(N, cons(M, L))) → min(cons(N, L))
ifmin(false, cons(N, cons(M, L))) → min(cons(M, L))
replace(N, M, nil) → nil
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L))
ifrepl(true, N, M, cons(K, L)) → cons(M, L)
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L))
selsort(nil) → nil
selsort(cons(N, L)) → ifselsort(eq(N, min(cons(N, L))), cons(N, L))
ifselsort(true, cons(N, L)) → cons(N, selsort(L))
ifselsort(false, cons(N, L)) → cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
ifmin(true, cons(x0, cons(x1, x2)))
ifmin(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
ifrepl(true, x0, x1, cons(x2, x3))
ifrepl(false, x0, x1, cons(x2, x3))
selsort(nil)
selsort(cons(x0, x1))
ifselsort(true, cons(x0, x1))
ifselsort(false, cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

IFMIN(false, cons(N, cons(M, L))) → MIN(cons(M, L))
IFMIN(true, cons(N, cons(M, L))) → MIN(cons(N, L))
MIN(cons(N, cons(M, L))) → IFMIN(le(N, M), cons(N, cons(M, L)))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
IFMIN(x1, x2) = x2
false = false
cons(x1, x2) = cons(x2)
MIN(x1) = MIN(x1)
true = true
le(x1, x2) = x1
0 = 0
s(x1) = s

Lexicographic path order with status [19].
Quasi-Precedence:

false > cons₁ > [MIN₁, true, 0]
s > [MIN₁, true, 0]

Status:

MIN₁: [1]
true: multiset
false: multiset
0: multiset
s: []
cons₁: [1]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(Y)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
le(0, Y) → true
le(s(X), 0) → false
le(s(X), s(Y)) → le(X, Y)
min(cons(0, nil)) → 0
min(cons(s(N), nil)) → s(N)
min(cons(N, cons(M, L))) → ifmin(le(N, M), cons(N, cons(M, L)))
ifmin(true, cons(N, cons(M, L))) → min(cons(N, L))
ifmin(false, cons(N, cons(M, L))) → min(cons(M, L))
replace(N, M, nil) → nil
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L))
ifrepl(true, N, M, cons(K, L)) → cons(M, L)
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L))
selsort(nil) → nil
selsort(cons(N, L)) → ifselsort(eq(N, min(cons(N, L))), cons(N, L))
ifselsort(true, cons(N, L)) → cons(N, selsort(L))
ifselsort(false, cons(N, L)) → cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
ifmin(true, cons(x0, cons(x1, x2)))
ifmin(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
ifrepl(true, x0, x1, cons(x2, x3))
ifrepl(false, x0, x1, cons(x2, x3))
selsort(nil)
selsort(cons(x0, x1))
ifselsort(true, cons(x0, x1))
ifselsort(false, cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

EQ(s(X), s(Y)) → EQ(X, Y)

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(Y)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
le(0, Y) → true
le(s(X), 0) → false
le(s(X), s(Y)) → le(X, Y)
min(cons(0, nil)) → 0
min(cons(s(N), nil)) → s(N)
min(cons(N, cons(M, L))) → ifmin(le(N, M), cons(N, cons(M, L)))
ifmin(true, cons(N, cons(M, L))) → min(cons(N, L))
ifmin(false, cons(N, cons(M, L))) → min(cons(M, L))
replace(N, M, nil) → nil
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L))
ifrepl(true, N, M, cons(K, L)) → cons(M, L)
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L))
selsort(nil) → nil
selsort(cons(N, L)) → ifselsort(eq(N, min(cons(N, L))), cons(N, L))
ifselsort(true, cons(N, L)) → cons(N, selsort(L))
ifselsort(false, cons(N, L)) → cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
ifmin(true, cons(x0, cons(x1, x2)))
ifmin(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
ifrepl(true, x0, x1, cons(x2, x3))
ifrepl(false, x0, x1, cons(x2, x3))
selsort(nil)
selsort(cons(x0, x1))
ifselsort(true, cons(x0, x1))
ifselsort(false, cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

EQ(s(X), s(Y)) → EQ(X, Y)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
EQ(x1, x2) = EQ(x2)
s(x1) = s(x1)

Lexicographic path order with status [19].
Quasi-Precedence:

s₁ > EQ₁

Status:

EQ₁: [1]
s₁: [1]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

                  ↳ QDP

                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(Y)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
le(0, Y) → true
le(s(X), 0) → false
le(s(X), s(Y)) → le(X, Y)
min(cons(0, nil)) → 0
min(cons(s(N), nil)) → s(N)
min(cons(N, cons(M, L))) → ifmin(le(N, M), cons(N, cons(M, L)))
ifmin(true, cons(N, cons(M, L))) → min(cons(N, L))
ifmin(false, cons(N, cons(M, L))) → min(cons(M, L))
replace(N, M, nil) → nil
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L))
ifrepl(true, N, M, cons(K, L)) → cons(M, L)
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L))
selsort(nil) → nil
selsort(cons(N, L)) → ifselsort(eq(N, min(cons(N, L))), cons(N, L))
ifselsort(true, cons(N, L)) → cons(N, selsort(L))
ifselsort(false, cons(N, L)) → cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
ifmin(true, cons(x0, cons(x1, x2)))
ifmin(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
ifrepl(true, x0, x1, cons(x2, x3))
ifrepl(false, x0, x1, cons(x2, x3))
selsort(nil)
selsort(cons(x0, x1))
ifselsort(true, cons(x0, x1))
ifselsort(false, cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IFREPL(false, N, M, cons(K, L)) → REPLACE(N, M, L)
REPLACE(N, M, cons(K, L)) → IFREPL(eq(N, K), N, M, cons(K, L))

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(Y)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
le(0, Y) → true
le(s(X), 0) → false
le(s(X), s(Y)) → le(X, Y)
min(cons(0, nil)) → 0
min(cons(s(N), nil)) → s(N)
min(cons(N, cons(M, L))) → ifmin(le(N, M), cons(N, cons(M, L)))
ifmin(true, cons(N, cons(M, L))) → min(cons(N, L))
ifmin(false, cons(N, cons(M, L))) → min(cons(M, L))
replace(N, M, nil) → nil
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L))
ifrepl(true, N, M, cons(K, L)) → cons(M, L)
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L))
selsort(nil) → nil
selsort(cons(N, L)) → ifselsort(eq(N, min(cons(N, L))), cons(N, L))
ifselsort(true, cons(N, L)) → cons(N, selsort(L))
ifselsort(false, cons(N, L)) → cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
ifmin(true, cons(x0, cons(x1, x2)))
ifmin(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
ifrepl(true, x0, x1, cons(x2, x3))
ifrepl(false, x0, x1, cons(x2, x3))
selsort(nil)
selsort(cons(x0, x1))
ifselsort(true, cons(x0, x1))
ifselsort(false, cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

IFREPL(false, N, M, cons(K, L)) → REPLACE(N, M, L)
REPLACE(N, M, cons(K, L)) → IFREPL(eq(N, K), N, M, cons(K, L))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
IFREPL(x1, x2, x3, x4) = x4
false = false
cons(x1, x2) = cons(x2)
REPLACE(x1, x2, x3) = REPLACE(x3)
eq(x1, x2) = x2
0 = 0
true = true
s(x1) = s

Lexicographic path order with status [19].
Quasi-Precedence:

cons₁ > [false, REPLACE₁, s]

Status:

REPLACE₁: [1]
true: multiset
false: multiset
0: multiset
s: []
cons₁: [1]

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ PisEmptyProof

                  ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(Y)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
le(0, Y) → true
le(s(X), 0) → false
le(s(X), s(Y)) → le(X, Y)
min(cons(0, nil)) → 0
min(cons(s(N), nil)) → s(N)
min(cons(N, cons(M, L))) → ifmin(le(N, M), cons(N, cons(M, L)))
ifmin(true, cons(N, cons(M, L))) → min(cons(N, L))
ifmin(false, cons(N, cons(M, L))) → min(cons(M, L))
replace(N, M, nil) → nil
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L))
ifrepl(true, N, M, cons(K, L)) → cons(M, L)
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L))
selsort(nil) → nil
selsort(cons(N, L)) → ifselsort(eq(N, min(cons(N, L))), cons(N, L))
ifselsort(true, cons(N, L)) → cons(N, selsort(L))
ifselsort(false, cons(N, L)) → cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
ifmin(true, cons(x0, cons(x1, x2)))
ifmin(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
ifrepl(true, x0, x1, cons(x2, x3))
ifrepl(false, x0, x1, cons(x2, x3))
selsort(nil)
selsort(cons(x0, x1))
ifselsort(true, cons(x0, x1))
ifselsort(false, cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

IFSELSORT(true, cons(N, L)) → SELSORT(L)
IFSELSORT(false, cons(N, L)) → SELSORT(replace(min(cons(N, L)), N, L))
SELSORT(cons(N, L)) → IFSELSORT(eq(N, min(cons(N, L))), cons(N, L))

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(Y)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
le(0, Y) → true
le(s(X), 0) → false
le(s(X), s(Y)) → le(X, Y)
min(cons(0, nil)) → 0
min(cons(s(N), nil)) → s(N)
min(cons(N, cons(M, L))) → ifmin(le(N, M), cons(N, cons(M, L)))
ifmin(true, cons(N, cons(M, L))) → min(cons(N, L))
ifmin(false, cons(N, cons(M, L))) → min(cons(M, L))
replace(N, M, nil) → nil
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L))
ifrepl(true, N, M, cons(K, L)) → cons(M, L)
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L))
selsort(nil) → nil
selsort(cons(N, L)) → ifselsort(eq(N, min(cons(N, L))), cons(N, L))
ifselsort(true, cons(N, L)) → cons(N, selsort(L))
ifselsort(false, cons(N, L)) → cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
ifmin(true, cons(x0, cons(x1, x2)))
ifmin(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
ifrepl(true, x0, x1, cons(x2, x3))
ifrepl(false, x0, x1, cons(x2, x3))
selsort(nil)
selsort(cons(x0, x1))
ifselsort(true, cons(x0, x1))
ifselsort(false, cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

IFSELSORT(true, cons(N, L)) → SELSORT(L)

The remaining pairs can at least be oriented weakly.

IFSELSORT(false, cons(N, L)) → SELSORT(replace(min(cons(N, L)), N, L))
SELSORT(cons(N, L)) → IFSELSORT(eq(N, min(cons(N, L))), cons(N, L))

Used ordering: Combined order from the following AFS and order.
IFSELSORT(x1, x2) = IFSELSORT(x2)
true = true
cons(x1, x2) = cons(x2)
SELSORT(x1) = SELSORT(x1)
false = false
replace(x1, x2, x3) = replace(x3)
min(x1) = x1
eq(x1, x2) = eq
0 = 0
le(x1, x2) = le(x1, x2)
s(x1) = x1
nil = nil
ifrepl(x1, x2, x3, x4) = ifrepl(x4)
ifmin(x1, x2) = ifmin(x2)

Lexicographic path order with status [19].
Quasi-Precedence:

false > [IFSELSORT₁, SELSORT_1] > [true, eq] > [cons₁, replace₁, 0, le₂, ifrepl₁, ifmin_1] > nil

Status:

ifrepl₁: [1]
IFSELSORT₁: [1]
eq: []
0: multiset
replace₁: [1]
nil: multiset
SELSORT₁: [1]
ifmin₁: [1]
true: multiset
false: multiset
le₂: [2,1]
cons₁: [1]

The following usable rules [14] were oriented:

replace(N, M, nil) → nil
ifrepl(true, N, M, cons(K, L)) → cons(M, L)
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L))
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

SELSORT(cons(N, L)) → IFSELSORT(eq(N, min(cons(N, L))), cons(N, L))
IFSELSORT(false, cons(N, L)) → SELSORT(replace(min(cons(N, L)), N, L))

The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(Y)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
le(0, Y) → true
le(s(X), 0) → false
le(s(X), s(Y)) → le(X, Y)
min(cons(0, nil)) → 0
min(cons(s(N), nil)) → s(N)
min(cons(N, cons(M, L))) → ifmin(le(N, M), cons(N, cons(M, L)))
ifmin(true, cons(N, cons(M, L))) → min(cons(N, L))
ifmin(false, cons(N, cons(M, L))) → min(cons(M, L))
replace(N, M, nil) → nil
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L))
ifrepl(true, N, M, cons(K, L)) → cons(M, L)
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L))
selsort(nil) → nil
selsort(cons(N, L)) → ifselsort(eq(N, min(cons(N, L))), cons(N, L))
ifselsort(true, cons(N, L)) → cons(N, selsort(L))
ifselsort(false, cons(N, L)) → cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
ifmin(true, cons(x0, cons(x1, x2)))
ifmin(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
ifrepl(true, x0, x1, cons(x2, x3))
ifrepl(false, x0, x1, cons(x2, x3))
selsort(nil)
selsort(cons(x0, x1))
ifselsort(true, cons(x0, x1))
ifselsort(false, cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

SELSORT(cons(N, L)) → IFSELSORT(eq(N, min(cons(N, L))), cons(N, L))
IFSELSORT(false, cons(N, L)) → SELSORT(replace(min(cons(N, L)), N, L))

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
SELSORT(x1) = SELSORT(x1)
cons(x1, x2) = cons(x2)
IFSELSORT(x1, x2) = x2
eq(x1, x2) = eq(x1, x2)
min(x1) = min
false = false
replace(x1, x2, x3) = x3
0 = 0
true = true
le(x1, x2) = le(x1)
s(x1) = s(x1)
nil = nil
ifrepl(x1, x2, x3, x4) = x4
ifmin(x1, x2) = x1

Lexicographic path order with status [19].
Quasi-Precedence:

cons₁ > SELSORT₁ > [eq₂, false, 0, true, nil]
cons₁ > min > le₁ > [eq₂, false, 0, true, nil]
cons₁ > s₁ > le₁ > [eq₂, false, 0, true, nil]

Status:

true: multiset
false: multiset
eq₂: [2,1]
min: []
0: multiset
s₁: [1]
le₁: [1]
cons₁: [1]
nil: multiset
SELSORT₁: [1]

The following usable rules [14] were oriented:

replace(N, M, nil) → nil
ifrepl(true, N, M, cons(K, L)) → cons(M, L)
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L))
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ EdgeDeletionProof

            ↳ QDP

              ↳ DependencyGraphProof

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPOrderProof

                      ↳ QDP

                        ↳ QDPOrderProof

                          ↳ QDP

                            ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

eq(0, 0) → true
eq(0, s(Y)) → false
eq(s(X), 0) → false
eq(s(X), s(Y)) → eq(X, Y)
le(0, Y) → true
le(s(X), 0) → false
le(s(X), s(Y)) → le(X, Y)
min(cons(0, nil)) → 0
min(cons(s(N), nil)) → s(N)
min(cons(N, cons(M, L))) → ifmin(le(N, M), cons(N, cons(M, L)))
ifmin(true, cons(N, cons(M, L))) → min(cons(N, L))
ifmin(false, cons(N, cons(M, L))) → min(cons(M, L))
replace(N, M, nil) → nil
replace(N, M, cons(K, L)) → ifrepl(eq(N, K), N, M, cons(K, L))
ifrepl(true, N, M, cons(K, L)) → cons(M, L)
ifrepl(false, N, M, cons(K, L)) → cons(K, replace(N, M, L))
selsort(nil) → nil
selsort(cons(N, L)) → ifselsort(eq(N, min(cons(N, L))), cons(N, L))
ifselsort(true, cons(N, L)) → cons(N, selsort(L))
ifselsort(false, cons(N, L)) → cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L)))

The set Q consists of the following terms:

eq(0, 0)
eq(0, s(x0))
eq(s(x0), 0)
eq(s(x0), s(x1))
le(0, x0)
le(s(x0), 0)
le(s(x0), s(x1))
min(cons(0, nil))
min(cons(s(x0), nil))
min(cons(x0, cons(x1, x2)))
ifmin(true, cons(x0, cons(x1, x2)))
ifmin(false, cons(x0, cons(x1, x2)))
replace(x0, x1, nil)
replace(x0, x1, cons(x2, x3))
ifrepl(true, x0, x1, cons(x2, x3))
ifrepl(false, x0, x1, cons(x2, x3))
selsort(nil)
selsort(cons(x0, x1))
ifselsort(true, cons(x0, x1))
ifselsort(false, cons(x0, x1))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.